/**
 * 
 */
package com.wachulski.marcin.msc.experiment;

import java.io.BufferedWriter;
import java.io.FileWriter;

import org.junit.Test;

import com.wachulski.marcin.msc.utils.FilePaths;

/**
 * @author Marcin Wachulski
 *
 */
public class DataGenerator {

	private static final int[] scDataSizeArray = { 
		20, 40, 60, 80, 100
	};
	
	@Test
	public final void genCdata() throws Exception {
		for (int dataSize : scDataSizeArray) {
			
			// data
			
			BufferedWriter writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/c/data_c_" + String.format("%05d", dataSize) + ".plm"));
			writer.write("; module-switching\n(IN-MODULE \"/PL-KERNEL-KB/PL-FOUNDATION/PL-SYSTEM/PL-BOUNDARY\")\n");
			writer.write("; assert\n(ASSERT ( AND\n\n");
			
			for (int i = 0; i < dataSize; i++)
				writer.write("\t(Being B" + (i+1) + ")\n");
			writer.write('\n');
			
			int chunks = dataSize/20;
			
			
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				//*
				writer.write("\t(c B"+(j+1)+" B"+(j+2)+")\n");
				writer.write("\t(c B"+(j+2)+" B"+(j+3)+")\n");
				writer.write("\t(c B"+(j+3)+" B"+(j+4)+")\n");
				writer.write("\t(c B"+(j+4)+" B"+(j+5)+")\n");
				writer.write("\t(c B"+(j+5)+" B"+(j+6)+")\n");
				writer.write("\t(c B"+(j+6)+" B"+(j+7)+")\n");
				writer.write("\t(c B"+(j+7)+" B"+(j+8)+")\n");
				writer.write("\t(c B"+(j+8)+" B"+(j+9)+")\n");
				writer.write("\t(c B"+(j+9)+" B"+(j+1)+")\n");
				//*/
				//*/
				writer.write("\t(j B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("\t(j B"+(j+2)+" B"+(j+2)+")\n");
				writer.write("\t(j B"+(j+3)+" B"+(j+3)+")\n");
				writer.write("\t(j B"+(j+4)+" B"+(j+4)+")\n");
				writer.write("\t(j B"+(j+5)+" B"+(j+5)+")\n");
				//*/
				//*
				writer.write("\t(j B"+(j+6)+" B"+(j+7)+")\n");
				writer.write("\t(j B"+(j+7)+" B"+(j+8)+")\n");
				writer.write("\t(j B"+(j+8)+" B"+(j+9)+")\n");
				writer.write("\t(j B"+(j+9)+" B"+(j+10)+")\n");
				writer.write("\t(j B"+(j+10)+" B"+(j+6)+")\n");
				//*/
				//*
				writer.write("\t(i B"+(j+11)+" B"+(j+12)+")\n");
				writer.write("\t(a B"+(j+13)+" B"+(j+14)+")\n");
				writer.write("\t(e B"+(j+15)+" B"+(j+16)+")\n");
				writer.write("\t(o B"+(j+17)+" B"+(j+18)+")\n");
				writer.write("\t(eq B"+(j+19)+" B"+(j+20)+")\n");
				writer.write("\t(j B"+(j+11)+" (ng B"+(j+20)+"))\n");
				//*/
				
				//*/
			}
			writer.write('\n');
			
			writer.write("\n))");
			writer.close();
			
			// exp script
			
			writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/c/exp_c_" + String.format("%05d", dataSize) + ".plm"));
			int t = 0;
			int k = 0;
			
			//* C1
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) (c ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(c Being_1 Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c Being_0 Being_0)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+2)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+3)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+4)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+9)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+11)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+12)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+13)+" B"+(j+13)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+14)+" B"+(j+14)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+15)+" B"+(j+15)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+16)+" B"+(j+16)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+17)+" B"+(j+17)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+18)+" B"+(j+18)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+19)+" B"+(j+19)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+20)+" B"+(j+20)+")\n");
				
			} //*/
				
			//* C2
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being))" +
				" (=> (AND (c ?x ?y)(c ?z ?x))(c ?z ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+1)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+1)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+1)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+1)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+1)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+1)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+1)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+9)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+9)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+9)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+9)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+9)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+9)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+9)+" B"+(j+8)+")\n");
			} //*/
				
			//* C3
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(<=> (j ?x ?x) (NOT (c ?x Being_0))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (c B"+(j+1)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (c B"+(j+2)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (c B"+(j+3)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (c B"+(j+4)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (c B"+(j+5)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (c B"+(j+6)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (c B"+(j+7)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (c B"+(j+8)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (c B"+(j+9)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (c B"+(j+10)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+9)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+10)+" B"+(j+10)+")\n");
			} //*/
				
			//* C4
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
						"(<=> (j ?x Being_1) (NOT (c ?x Being_0))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+10)+")\n");
			} //*/
				
			//* C5
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(j Being_1 Being_1)\n");
			//*/
				
			//* C6
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
						"(<=> (j ?x Being_1) (j ?x ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+9)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+10)+")\n");
			} //*/
				
			//* C7
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					" (<=> (j ?x ?y)(AND (j ?x Being_1)(c ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
					
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+6)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+7)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+8)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+9)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+10)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+10)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+10)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+10)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+10)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+10)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+10)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+10)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+10)+" B"+(j+9)+")\n");
			} //*/
				
			//* C8
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					" (<=> (j ?x ?y)(AND (j ?x ?x)(c ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+9)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+2)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+3)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+10)+")\n");
			} //*/
				
			//* C9
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(REFUTATION-QUERY (FORALL ((?x Being)) (NOT (j Being_0 ?x))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;	
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 Being_1))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+1)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+2)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+3)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+4)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+5)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+6)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+7)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+8)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+9)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+10)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+11)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+12)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+13)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+14)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+15)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+16)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+17)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+18)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+19)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 "+" B"+(j+20)+"))\n");
			} //*/
				
			//* C10
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(REFUTATION-QUERY (FORALL ((?x Being)) (NOT (j ?x Being_0))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
					
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_0 Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_1 Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j B"+(j+1)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j B"+(j+2)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j B"+(j+3)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j B"+(j+4)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j B"+(j+5)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j B"+(j+6)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j B"+(j+7)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j B"+(j+8)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j B"+(j+9)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j B"+(j+10)+" Being_0))\n");
			} //*/
				
			//* C11
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (j ?x ?y)(AND (j ?x Being_1)(j ?y Being_1))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(j Being_1 Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+10)+")\n");
			} //*/
			
			//* C12
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (c ?x ?y)(FORALL ((?z Being)) (=> (j ?z ?x)(j ?z ?y)))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (j Being_0 Being_0)(j Being_0 Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (j Being_1 Being_1)(j Being_1 Being_1))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (j B"+(j+1)+" B"+(j+1)+")(j B"+(j+1)+" B"+(j+2)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (j B"+(j+2)+" B"+(j+1)+")(j B"+(j+2)+" B"+(j+2)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (j B"+(j+3)+" B"+(j+1)+")(j B"+(j+3)+" B"+(j+2)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (j B"+(j+4)+" B"+(j+1)+")(j B"+(j+4)+" B"+(j+2)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (j B"+(j+5)+" B"+(j+1)+")(j B"+(j+5)+" B"+(j+2)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (j B"+(j+1)+" B"+(j+9)+")(j B"+(j+1)+" B"+(j+6)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (j B"+(j+2)+" B"+(j+9)+")(j B"+(j+2)+" B"+(j+6)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (j B"+(j+3)+" B"+(j+9)+")(j B"+(j+3)+" B"+(j+6)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (j B"+(j+4)+" B"+(j+9)+")(j B"+(j+4)+" B"+(j+6)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (j B"+(j+5)+" B"+(j+9)+")(j B"+(j+5)+" B"+(j+6)+"))\n");
			} //*/
			
			//* C13
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being)) " +
					"(=> (AND (j ?x ?y)(j ?z ?x))(j ?z ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+9)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+6)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+7)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+6)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+9)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+9)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+8)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+8)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+7)+" B"+(j+6)+")\n");
			} //*/
			
			//* C14
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (i ?x ?y)(i ?y ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+11)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+12)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+7)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+9)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+6)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+7)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+6)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+8)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+8)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+7)+" B"+(j+8)+")\n");
			} //*/
			
			//* C15
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (e ?x ?y)(e ?y ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(e B"+(j+15)+" B"+(j+16)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(e B"+(j+16)+" B"+(j+15)+")\n");
			} //*/
			
			//* C16
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(a ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+2)+" B"+(j+2)+")\n");
			} //*/
			
			//* C17
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(=> (j ?x Being_1)(i ?x ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+2)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+3)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+4)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+9)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+10)+" B"+(j+10)+")\n");
			} //*/
			
			//* C18
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (j ?x ?y)(i ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+6)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+7)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+8)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+9)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+6)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+7)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+8)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+7)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+8)+" B"+(j+10)+")\n");
			} //*/
			
			//* C19
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (c ?x ?y)(a ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+1)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+2)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+3)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+4)+" B"+(j+5)+")\n");
			} //*/
			
			//* C20
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (j ?x ?y)(a ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+2)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+3)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+4)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+5)+" B"+(j+5)+")\n");
			} //*/
			
			//* C21
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (e ?x ?y)(NOT (i ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (i B"+(j+15)+" B"+(j+16)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (i B"+(j+16)+" B"+(j+15)+"))\n");
			} //*/
			
			//* C22
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (o ?x ?y)(NOT (a ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (a B"+(j+17)+" B"+(j+18)+"))\n");
			} //*/
			
			//* C23
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (j ?x (ng ?y))(NOT (j ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j B"+(j+11)+" B"+(j+20)+"))\n");
			} //*/
			
			//* C24
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (j ?x (ng ?y))(NOT (j Being_1 ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (j Being_1 B"+(j+20)+"))\n");
			} //*/
			
			//* C25
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (e ?x (ng ?y))(a ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(e B"+(j+13)+" (ng B"+(j+14)+"))\n");
			} //*/
			
			writer.close();
			
		}
	}

	@Test
	public final void genPdata() throws Exception {
		for (int dataSize : scDataSizeArray) {
			
			// data
			
			BufferedWriter writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/p/data_p_" + String.format("%05d", dataSize) + ".plm"));
			writer.write("; module-switching\n(IN-MODULE \"/PL-KERNEL-KB/PL-FOUNDATION/PL-SYSTEM/PL-BOUNDARY\")\n");
			writer.write("; assert\n(ASSERT ( AND\n\n");
			
			for (int i = 0; i < dataSize; i++)
				writer.write("\t(Being B" + (i+1) + ")\n");
			writer.write('\n');
			
			int chunks = dataSize/20;
			
			
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				//*
				writer.write("\t(j B"+(j+1)+" B"+(j+2)+")\n");
				writer.write("\t(j B"+(j+2)+" B"+(j+3)+")\n");
				writer.write("\t(j B"+(j+3)+" B"+(j+4)+")\n");
				writer.write("\t(j B"+(j+4)+" B"+(j+5)+")\n");
				writer.write("\t(j B"+(j+5)+" B"+(j+1)+")\n");
				//*/
				//*/
				writer.write("\t(j B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("\t(j B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("\t(j B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("\t(j B"+(j+9)+" B"+(j+9)+")\n");
				//*/
				//*
				writer.write("\t(i B"+(j+10)+" B"+(j+11)+")\n");
				writer.write("\t(a B"+(j+12)+" B"+(j+13)+")\n");
				writer.write("\t(e B"+(j+14)+" B"+(j+15)+")\n");
				writer.write("\t(o B"+(j+16)+" B"+(j+17)+")\n");
				writer.write("\t(eq B"+(j+18)+" B"+(j+19)+")\n");
				writer.write("\t(eq B"+(j+18)+" B"+(j+20)+")\n");
				//*/
				
				//*/
			}
			writer.write('\n');
			
			writer.write("\n))");
			writer.close();
			
			// exp script
			
			writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/p/exp_p_" + String.format("%05d", dataSize) + ".plm"));
			int t = 0;
			int k = 0;
			
			//* P1
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) (j ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j Being_1 Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+2)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+3)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+9)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+11)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+12)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+13)+" B"+(j+13)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+14)+" B"+(j+14)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+15)+" B"+(j+15)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+16)+" B"+(j+16)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+17)+" B"+(j+17)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+18)+" B"+(j+18)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+19)+" B"+(j+19)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+20)+" B"+(j+20)+")\n");
				
			} //*/
				
			//* P2
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being))" +
				" (=> (AND (j ?x ?y)(j ?z ?x))(j ?z ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+2)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+2)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+3)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+3)+" B"+(j+2)+")\n");
			} //*/
				
			//* P3
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(j ?x Being_1))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j Being_1 Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+2)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+3)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+6)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+7)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+8)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+9)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+10)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+11)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+12)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+13)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+14)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+15)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+16)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+17)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+18)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+19)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+20)+" Being_1)\n");
			} //*/
				
			//* P4
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?y Being)) (FORALL ((?x Being)) " +
					"(j ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+1)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+2)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+3)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+4)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+5)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+6)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+7)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+8)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+9)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+10)+"))\n");
			} //*/
			
			//* P5
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (i ?x ?y)(i ?y ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+10)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+11)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+1)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+1)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+1)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+2)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+2)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+3)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+5)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+5)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+5)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+5)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+4)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+4)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+4)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+3)+" B"+(j+2)+")\n");
			} //*/
			
			//* P6
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (e ?x ?y)(e ?y ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(e B"+(j+14)+" B"+(j+15)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(e B"+(j+15)+" B"+(j+14)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(e B"+(j+3)+" B"+(j+7)+")\n");
				
			} //*/
			
			//* P7
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(a ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(a Being_1 Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+2)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+3)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+4)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+9)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+11)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+12)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+13)+" B"+(j+13)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+14)+" B"+(j+14)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+15)+" B"+(j+15)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+16)+" B"+(j+16)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+17)+" B"+(j+17)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+18)+" B"+(j+18)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+19)+" B"+(j+19)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+20)+" B"+(j+20)+")\n");
				
			} //*/
			
			//* P8
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(i ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(i Being_1 Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+2)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+3)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+4)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+9)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+11)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+12)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+13)+" B"+(j+13)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+14)+" B"+(j+14)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+15)+" B"+(j+15)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+16)+" B"+(j+16)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+17)+" B"+(j+17)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+18)+" B"+(j+18)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+19)+" B"+(j+19)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+20)+" B"+(j+20)+")\n");
				
			} //*/
			
			//* P9
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (e ?x ?y)(NOT (i ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (i B"+(j+14)+" B"+(j+15)+"))\n");
				
			} //*/
			
			//* P10
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (o ?x ?y)(NOT (a ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (a B"+(j+16)+" B"+(j+17)+"))\n");
				
			} //*/
			
			//* P11
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?m Being)) " +
					"(=> (AND (a ?m ?y)(i ?m ?x))(i ?x ?y)))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				
			} //*/
			
			//* P12
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?m Being)) " +
					"(=> (AND (a ?m ?y)(a ?x ?m))(a ?x ?y)))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
			} //*/
			
			writer.close();
			
		}
	}
	
	@Test
	public final void genKdata() throws Exception {
		for (int dataSize : scDataSizeArray) {
			
			// data
			
			BufferedWriter writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/k/data_k_" + String.format("%05d", dataSize) + ".plm"));
			writer.write("; module-switching\n(IN-MODULE \"/PL-KERNEL-KB/PL-FOUNDATION/PL-SYSTEM/PL-BOUNDARY\")\n");
			writer.write("; assert\n(ASSERT ( AND\n\n");
			
			for (int i = 0; i < dataSize; i++)
				writer.write("\t(Being B" + (i+1) + ")\n");
			writer.write('\n');
			
			int chunks = dataSize/20;
			
			
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				//*
				writer.write("\t(j B"+(j+1)+" B"+(j+2)+")\n");
				writer.write("\t(j B"+(j+2)+" B"+(j+3)+")\n");
				writer.write("\t(j B"+(j+3)+" B"+(j+4)+")\n");
				writer.write("\t(j B"+(j+4)+" B"+(j+5)+")\n");
				writer.write("\t(j B"+(j+5)+" B"+(j+1)+")\n");
				//*/
				//*/
				writer.write("\t(j B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("\t(j B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("\t(j B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("\t(j B"+(j+9)+" B"+(j+9)+")\n");
				//*/
				//*
				writer.write("\t(i B"+(j+10)+" B"+(j+11)+")\n");
				writer.write("\t(a B"+(j+12)+" B"+(j+13)+")\n");
				writer.write("\t(e B"+(j+14)+" B"+(j+15)+")\n");
				writer.write("\t(o B"+(j+16)+" B"+(j+17)+")\n");
				writer.write("\t(eq B"+(j+18)+" B"+(j+19)+")\n");
				writer.write("\t(eq B"+(j+18)+" B"+(j+20)+")\n");
				//*/
				
				//*/
			}
			writer.write('\n');
			
			writer.write("\n))");
			writer.close();
			
			// exp script
			
			writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/k/exp_k_" + String.format("%05d", dataSize) + ".plm"));
			int t = 0;
			int k = 0;
			
			//* K1
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) (j ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+2)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+3)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+9)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+11)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+12)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+13)+" B"+(j+13)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+14)+" B"+(j+14)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+15)+" B"+(j+15)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+16)+" B"+(j+16)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+17)+" B"+(j+17)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+18)+" B"+(j+18)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+19)+" B"+(j+19)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+20)+" B"+(j+20)+")\n");
				
			} //*/
				
			//* K2
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being))" +
				" (=> (AND (j ?x ?y)(j ?z ?x))(j ?z ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+2)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+2)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+3)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+3)+" B"+(j+2)+")\n");
			} //*/
			
			//* K3
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (i ?x ?y)(i ?y ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+10)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+11)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+1)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+1)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+1)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+2)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+2)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+3)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+5)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+5)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+5)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+5)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+4)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+4)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+4)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+3)+" B"+(j+2)+")\n");
			} //*/
			
			//* K4
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (e ?x ?y)(e ?y ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(e B"+(j+14)+" B"+(j+15)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(e B"+(j+15)+" B"+(j+14)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(e B"+(j+3)+" B"+(j+7)+")\n");
				
			} //*/
			
			//* K5
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (j ?x ?y)(a ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+1)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+2)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+3)+" B"+(j+4)+")\n");
				
			} //*/
			
			//* K6
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(a ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+2)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+3)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+4)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a B"+(j+5)+" B"+(j+5)+")\n");

			} //*/
			
			//* K7
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(i ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+2)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+3)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+4)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+9)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+11)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+12)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+13)+" B"+(j+13)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+14)+" B"+(j+14)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+15)+" B"+(j+15)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+16)+" B"+(j+16)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+17)+" B"+(j+17)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+18)+" B"+(j+18)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+19)+" B"+(j+19)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i B"+(j+20)+" B"+(j+20)+")\n");
				
			} //*/
			
			//* K8
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (e ?x ?y)(NOT (i ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (i B"+(j+14)+" B"+(j+15)+"))\n");
				
			} //*/
			
			//* K9
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (o ?x ?y)(NOT (a ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (a B"+(j+16)+" B"+(j+17)+"))\n");
				
			} //*/
			
			//* K10
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?m Being)) " +
					"(=> (AND (a ?m ?y)(i ?m ?x))(i ?x ?y)))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				
			} //*/
			
			//* K11
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?m Being)) " +
					"(=> (AND (a ?m ?y)(a ?x ?m))(a ?x ?y)))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
			} //*/
			
			writer.close();
			
		}
	}

	@Test
	public final void genLdata() throws Exception {
		for (int dataSize : scDataSizeArray) {
			
			// data
			
			BufferedWriter writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/l/data_l_" + String.format("%05d", dataSize) + ".plm"));
			writer.write("; module-switching\n(IN-MODULE \"/PL-KERNEL-KB/PL-FOUNDATION/PL-SYSTEM/PL-BOUNDARY\")\n");
			writer.write("; assert\n(ASSERT ( AND\n\n");
			
			for (int i = 0; i < dataSize; i++)
				writer.write("\t(Being B" + (i+1) + ")\n");
			writer.write('\n');
			
			int chunks = dataSize/20;
			
			
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				//*
				writer.write("\t(j B"+(j+1)+" B"+(j+2)+")\n");
				writer.write("\t(j B"+(j+2)+" B"+(j+3)+")\n");
				writer.write("\t(j B"+(j+3)+" B"+(j+1)+")\n");
				writer.write("\t(j B"+(j+3)+" B"+(j+4)+")\n");
				writer.write("\t(j B"+(j+4)+" Being_U)\n");
				writer.write("\t(j B"+(j+5)+" Being_U)\n");
				writer.write("\t(j B"+(j+4)+" B"+(j+5)+")\n");
				//*/
				writer.write("\t(eps B"+(j+6)+" B"+(j+7)+")\n");
				writer.write("\t(eps B"+(j+7)+" B"+(j+8)+")\n");
				writer.write("\t(eps B"+(j+8)+" B"+(j+6)+")\n");
				writer.write("\t(j B"+(j+9)+" Being_P)\n");
				writer.write("\t(j B"+(j+10)+" Being_P)\n");
				//*
				writer.write("\t(I B"+(j+11)+" B"+(j+12)+")\n");
				writer.write("\t(A B"+(j+13)+" B"+(j+14)+")\n");
				writer.write("\t(E B"+(j+15)+" B"+(j+16)+")\n");
				writer.write("\t(O B"+(j+17)+" B"+(j+18)+")\n");
				writer.write("\t(eq_ B"+(j+19)+" B"+(j+20)+")\n");
				writer.write("\t(j B"+(j+11)+" (ng_ B"+(j+20)+"))\n");
				//*/
				
				//*/
			}
			writer.write('\n');
			
			writer.write("\n))");
			writer.close();
			
			// exp script
			
			writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/l/exp_l_" + String.format("%05d", dataSize) + ".plm"));
			int t = 0;
			int k = 0;
			
			//* C48
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?z Being)) " +
					"(=> (AND (j ?x Being_U)(j ?z ?x))(j ?x ?z)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" Being_U)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" Being_U)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+4)+")\n");
			} //*/
			
			//* C49
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?z Being)) " +
					"(=> (AND (j ?x Being_U)(j ?z ?x))(j ?z Being_U)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+4)+" Being_U)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" Being_U)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+3)+" Being_U)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+2)+" Being_U)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" Being_U)\n");
			} //*/
			
			//* C50
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(<=> (j ?x Being_U)(FORALL ((?z Being)(?u Being)) " +
					"(=> (AND (j ?z ?x)(j ?u ?x))(j ?z ?u)))))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
			} //*/
			
			//* L1
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> " +
						"(FORALL ((?z Being)) (=> (j ?z ?x)(j ?z ?y)))" +
						"(FORALL ((?z Being)) (=> (AND (j ?z Being_U)(j ?z ?x))(j ?z ?y)))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;

				writer.write("; "+t+"-"+(k++)+"\n\t(AND (j B"+(j+4)+" B"+(j+4)+")(j B"+(j+4)+" Being_U))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(AND (j B"+(j+5)+" B"+(j+5)+")(j B"+(j+5)+" Being_U))\n");
			} //*/
			
			//* L2
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> " +
						"(FORALL ((?z Being)) (=> (j ?z ?x)(j ?z ?y)))" +
						"(FORALL ((?z Being)) (=> (eps ?z ?x)(eps ?z ?y)))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
					
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+6)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+7)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+8)+" B"+(j+6)+")\n");
			} //*/
			
			//* L3
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(<=> (eps ?x Being_V)(j ?x Being_U)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;

				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+4)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+5)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+4)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+5)+" B"+(j+5)+")\n");
			} //*/
			
			//* L4
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being)) " +
					"(=> (AND (eps ?x ?y)(eps ?z ?x))(eps ?z ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;

				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+6)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+7)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+8)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+7)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+8)+" B"+(j+7)+")\n");
			} //*/
			
			//* L5
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (eps ?x ?y)(eps ?x ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;

				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+4)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+8)+" B"+(j+8)+")\n");
			} //*/
			
			//* L6
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?z Being)) " +
					"(=> (AND (eps ?x ?x)(eps ?z ?x))(eps ?x ?z)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;

				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+4)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+5)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+7)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+8)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+6)+" B"+(j+8)+")\n");
			} //*/
			
			//* L7
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(=> (eps ?x ?x)" +
						"(FORALL ((?z Being)(?u Being)) " +
							"(=> (AND (eps ?z ?x)(eps ?u ?x))(eps ?z ?u)))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;

			} //*/
			
			//* L8
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (AND (eps ?x ?y)" +
					"	(AND (EXISTS ((?z Being)) (eps ?z ?x))" +
					"		(FORALL ((?z Being)(?u Being)) " +
								"(=> (AND (eps ?z ?x)(eps ?u ?x))(eps ?z ?u)))" +
					"		(FORALL ((?z Being)) (=> (eps ?z ?x)(eps ?z ?y)))))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;

			} //*/
			
			//* L9
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being))" +
					"(<=> (j ?x Being_P)(AND (j ?x ?x)(NOT (eps ?x ?x)))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(AND (j B"+(j+9)+" B"+(j+9)+")" +
						"(NOT (eps B"+(j+9)+" B"+(j+9)+")))\n");
			} //*/
			
			//* L10
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being))" +
					"(<=> (j ?x Being_P)(AND (j ?x ?x)(NOT (j ?x Being_U)))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(AND (j B"+(j+9)+" B"+(j+9)+")" +
						"(NOT (eps B"+(j+9)+" Being_U)))\n");
			} //*/
			
			//* L11
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being))" +
					"(<=> (j ?x Being_1)(OR (eps ?x Being_V)(j ?x Being_P))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
			} //*/
			
			//* L12
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					"(<=> (c_ ?x ?y)(c ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
			} //*/
			
			//* L13
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					"(<=> (eps ?x ?y)" +
					"	(AND (eps ?x ?x)" +
					"		(FORALL ((?z Being)) (=> (eps ?z ?x)(eps ?z ?y))))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+7)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+6)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+8)+" B"+(j+7)+")\n");
				
			} //*/
			
			//* L14
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					"(<=> (eps ?x ?y)(AND (eps ?x Being_V)(c_ ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+6)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+7)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+8)+" Being_V)\n");
				
			} //*/
			
			//* L15
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					"(<=> (eps ?x ?y)(AND (j ?x Being_U)(c ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+6)+" Being_U)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+7)+" Being_U)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+8)+" Being_U)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+6)+" B"+(j+7)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(c B"+(j+7)+" B"+(j+8)+")\n");
				
			} //*/
			
			//* L16
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?z Being))" +
					"(=> (AND (eps ?x Being_V)(eps ?z ?x))(eps ?x ?z)))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (eps B"+(j+6)+" Being_V)(eps B"+(j+7)+" B"+(j+6)+"))" +
						"(eps B"+(j+6)+" B"+(j+7)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (eps B"+(j+8)+" Being_V)(eps B"+(j+6)+" B"+(j+8)+"))" +
						"(eps B"+(j+8)+" B"+(j+6)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (eps B"+(j+6)+" Being_V)(eps B"+(j+5)+" B"+(j+6)+"))" +
						"(eps B"+(j+6)+" B"+(j+5)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (eps B"+(j+6)+" Being_V)(eps B"+(j+11)+" B"+(j+6)+"))" +
						"(eps B"+(j+6)+" B"+(j+11)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (eps B"+(j+6)+" Being_V)(eps B"+(j+20)+" B"+(j+6)+"))" +
						"(eps B"+(j+6)+" B"+(j+20)+"))\n");
				
			} //*/
			
			//* L17
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					"(=> (eps ?x ?y)(<=> (eps ?y Being_V)(eps ?y ?x))))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+6)+" Being_V) (eps B"+(j+7)+" B"+(j+6)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+6)+" Being_V) (eps B"+(j+8)+" B"+(j+6)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+7)+" Being_V) (eps B"+(j+8)+" B"+(j+7)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+7)+" Being_V) (eps B"+(j+6)+" B"+(j+7)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+8)+" Being_V) (eps B"+(j+6)+" B"+(j+8)+"))\n");
			} //*/
			
			//* L18
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					"(=> (eps ?x ?y)(a_ ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
			} //*/
			
			//* L19
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					"(<=> (AND (eps ?x Being_V)(a_ ?x ?y))(eps ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
			} //*/
			
			//* L20
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being))" +
					"(=> (eps ?x Being_V)(FORALL ((?y Being)) (<=>(c_ ?x ?y)(a_ ?x ?y)))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
			} //*/
			
			//* L21
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (a ?x ?y)(a_ ?x ?y)))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (a B"+(j+6)+" B"+(j+7)+")(a_ B"+(j+6)+" B"+(j+7)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (a B"+(j+7)+" B"+(j+8)+")(a_ B"+(j+7)+" B"+(j+8)+"))\n");
			} //*/
			
			//* L22
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being))" +
					"(=> (eps ?x Being_V)(FORALL ((?y Being)) (<=>(a ?x ?y)(a_ ?x ?y)))))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (eps B"+(j+6)+" Being_V)" +
						"(<=> (a B"+(j+6)+" B"+(j+7)+")(a_ B"+(j+6)+" B"+(j+7)+")))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (eps B"+(j+7)+" Being_V)" +
						"(<=> (a B"+(j+7)+" B"+(j+8)+")(a_ B"+(j+7)+" B"+(j+8)+")))\n");
			} //*/
			
			//* L23
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(a_ ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+6)+" B"+(j+6)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+7)+" B"+(j+7)+")\n");
			} //*/
			
			//* L24
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(=> (eps ?x Being_V)(i_ ?x ?x)))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (eps B"+(j+6)+" Being_V)(i_ B"+(j+6)+" B"+(j+6)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (eps B"+(j+7)+" Being_V)(i_ B"+(j+7)+" B"+(j+7)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (eps B"+(j+8)+" Being_V)(i_ B"+(j+8)+" B"+(j+8)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (eps B"+(j+9)+" Being_V)(i_ B"+(j+9)+" B"+(j+9)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (eps B"+(j+10)+" Being_V)(i_ B"+(j+10)+" B"+(j+10)+"))\n");
			} //*/
			
			//* L25
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					"(<=> (e_ ?x ?y)(NOT (i_ ?x ?y))))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (e_ B"+(j+15)+" B"+(j+16)+")(NOT (i_ B"+(j+15)+" B"+(j+16)+")))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (e_ B"+(j+17)+" B"+(j+18)+")(NOT (i_ B"+(j+17)+" B"+(j+18)+")))\n");
			} //*/
			
			//* L26
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					"(<=> (o_ ?x ?y)(NOT (a_ ?x ?y))))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (o_ B"+(j+17)+" B"+(j+18)+")(NOT (a_ B"+(j+15)+" B"+(j+16)+")))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (o_ B"+(j+1)+" B"+(j+2)+")(NOT (a_ B"+(j+1)+" B"+(j+2)+")))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (o_ B"+(j+6)+" B"+(j+7)+")(NOT (a_ B"+(j+6)+" B"+(j+7)+")))\n");
			} //*/
			
			//* L27
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					"(<=> (i_ ?x ?y)(i_ ?y ?x)))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (i_ B"+(j+11)+" B"+(j+12)+")(i_ B"+(j+12)+" B"+(j+11)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (i_ B"+(j+13)+" B"+(j+14)+")(i_ B"+(j+14)+" B"+(j+13)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (i_ B"+(j+1)+" B"+(j+2)+")(i_ B"+(j+2)+" B"+(j+1)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (i_ B"+(j+6)+" B"+(j+7)+")(i_ B"+(j+7)+" B"+(j+6)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (i_ B"+(j+7)+" B"+(j+8)+")(i_ B"+(j+8)+" B"+(j+7)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (i_ B"+(j+6)+" B"+(j+8)+")(i_ B"+(j+8)+" B"+(j+6)+"))\n");
			} //*/
			
			//* L28
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					"(<=> (e_ ?x ?y)(e_ ?y ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
			} //*/
			
			//* L29
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					"(=> (eps ?x Being_V)(<=> (eq ?x ?y)(eq_ ?x ?y))))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
			} //*/
			
			//* L30
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					"(<=> (e_ ?x (ng_ ?y))(a_ ?x ?y)))\n");
			/*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
			} //*/
			
			writer.close();
		}
	}

	@Test
	public final void genLPdata() throws Exception {
		for (int dataSize : scDataSizeArray) {
			
			// data
			
			BufferedWriter writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/lp/data_lp_" + String.format("%05d", dataSize) + ".plm"));
			writer.write("; module-switching\n(IN-MODULE \"/PL-KERNEL-KB/PL-FOUNDATION/PL-SYSTEM/PL-BOUNDARY\")\n");
			writer.write("; assert\n(ASSERT ( AND\n\n");
			
			for (int i = 0; i < dataSize; i++)
				writer.write("\t(Being B" + (i+1) + ")\n");
			writer.write('\n');
			
			int chunks = dataSize/20;
			
			
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				//*
				writer.write("\t(j B"+(j+1)+" B"+(j+2)+")\n");
				writer.write("\t(j B"+(j+2)+" B"+(j+3)+")\n");
				writer.write("\t(j B"+(j+3)+" B"+(j+1)+")\n");
				writer.write("\t(j B"+(j+4)+" Being_U)\n");
				writer.write("\t(eps B"+(j+5)+" Being_U)\n");
				writer.write("\t(j B"+(j+6)+" Being_V)\n");
				writer.write("\t(eps B"+(j+7)+" Being_V)\n");
				writer.write("\t(j B"+(j+8)+" Being_P)\n");
				writer.write("\t(eps B"+(j+9)+" Being_P)\n");
				writer.write("\t(eps B"+(j+10)+" B"+(j+11)+")\n");
				writer.write("\t(eps B"+(j+11)+" B"+(j+12)+")\n");
				writer.write("\t(eps B"+(j+12)+" B"+(j+10)+")\n");
				writer.write("\t(eps B"+(j+13)+" B"+(j+13)+")\n");
				writer.write("\t(eps B"+(j+14)+" B"+(j+14)+")\n");
				writer.write("\t(i_ B"+(j+15)+" B"+(j+16)+")\n");
				writer.write("\t(a_ B"+(j+17)+" B"+(j+18)+")\n");
				writer.write("\t(e_ B"+(j+19)+" B"+(j+20)+")\n");
				writer.write("\t(o_ B"+(j+1)+" B"+(j+2)+")\n");
				//*/
				
				//*/
			}
			writer.write('\n');
			
			writer.write("\n))");
			writer.close();
			
			// exp script
			
			writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/lp/exp_lp_" + String.format("%05d", dataSize) + ".plm"));
			int t = 0;
			int k = 0;
			
			//* LP1
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) (j ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j Being_1 Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j Being_V Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j Being_P Being_P)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j Being_U Being_U)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+10)+" B"+(j+10)+")\n");
				
			} //*/
				
			//* LP2
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being))" +
				" (=> (AND (j ?x ?y)(j ?z ?x))(j ?z ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+2)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+3)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+10)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+12)+" B"+(j+11)+")\n");
			} //*/
				
			//* LP3
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(j ?x Being_1))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j Being_V Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j Being_P Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j Being_U Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" Being_1)\n");
			} //*/
				
			//* LP4
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?y Being)) (FORALL ((?x Being)) " +
					"(j ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+1)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+5)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+10)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+15)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (j ?x B"+(j+20)+"))\n");
			} //*/
			
			//* LP5
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?z Being)) " +
					"(=> (AND (j ?x Being_U)(j ?z ?x))(j ?x ?z)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+1)+" Being_U)(j B"+(j+2)+" B"+(j+1)+"))" +
						"(j B"+(j+1)+" B"+(j+2)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+4)+" Being_U)(j B"+(j+5)+" B"+(j+4)+"))" +
						"(j B"+(j+4)+" B"+(j+5)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+10)+" Being_U)(j B"+(j+3)+" B"+(j+10)+"))" +
						"(j B"+(j+10)+" B"+(j+3)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+9)+" Being_U)(j B"+(j+17)+" B"+(j+9)+"))" +
						"(j B"+(j+9)+" B"+(j+17)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+5)+" Being_U)(j B"+(j+5)+" B"+(j+5)+"))" +
						"(j B"+(j+5)+" B"+(j+5)+"))\n");
				
			} //*/
			
			//* LP6
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?z Being)) " +
					"(=> (AND (j ?x Being_U)(j ?z ?x))(j ?z Being_U)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+1)+" Being_U)(j B"+(j+2)+" B"+(j+1)+"))" +
						"(j B"+(j+2)+" Being_U))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+4)+" Being_U)(j B"+(j+5)+" B"+(j+4)+"))" +
						"(j B"+(j+5)+" Being_U))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+10)+" Being_U)(j B"+(j+3)+" B"+(j+10)+"))" +
						"(j B"+(j+3)+" Being_U))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+9)+" Being_U)(j B"+(j+17)+" B"+(j+9)+"))" +
						"(j B"+(j+17)+" Being_U))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+5)+" Being_U)(j B"+(j+5)+" B"+(j+5)+"))" +
						"(j B"+(j+5)+" Being_U))\n");
				
			} //*/
			
			//* LP7
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(<=> (j ?x Being_U)" +
					"	(FORALL ((?z Being)(?u Being)) (=> (AND(j ?z ?x)(j ?u ?x))(j ?z ?u)))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(j ?z B"+(j+4)+")(j ?u B"+(j+4)+"))(j ?z ?u)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(j ?z B"+(j+5)+")(j ?u B"+(j+5)+"))(j ?z ?u)))\n");
				
				
			} //*/
			
			//* LP8
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(EXISTS ((?z Being)) (eps ?z ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (eps ?x B"+(j+1)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (eps ?x B"+(j+5)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (eps ?x B"+(j+10)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (eps ?x B"+(j+15)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(EXISTS ((?x Being)) (eps ?x B"+(j+20)+"))\n");
				
			} //*/
			
			//* LP9
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (FORALL ((?z Being)) (=> (j ?z ?x)(j ?z ?y)))" +
					"		(FORALL ((?z Being)) (=> (eps ?z ?x)(eps ?z ?y)))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
			} //*/
			
			//* LP10
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(<=> (eps ?x Being_V)(j ?x Being_U)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+4)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+5)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+7)+" Being_U)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+20)+" Being_V)(j B"+(j+20)+" Being_U))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+6)+" Being_V)(j B"+(j+6)+" Being_U))\n");
				
			} //*/
			
			//* LP11
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being)) " +
					"(=> (AND (eps ?x ?y)(eps ?z ?x))(eps ?z ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+10)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+12)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+11)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+12)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+10)+" B"+(j+10)+")\n");
				
			} //*/
			
			//* LP12
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (eps ?x ?y)(eps ?x ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+11)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+12)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+7)+" B"+(j+7)+")\n");
				
			} //*/
			
			//* LP13
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being)) " +
					"(=> (AND (eps ?x ?x)(eps ?z ?x))(eps ?x ?z)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+10)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+12)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+11)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+12)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+10)+" B"+(j+10)+")\n");
				
			} //*/
			
			//* LP14
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being)) " +
					"(=> (eps ?x ?x)" +
					"(FORALL ((?z Being)(?u Being)) (=> (AND(eps ?z ?x)(eps ?u ?x))(eps ?z ?u)))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(eps ?z B"+(j+5)+")(eps ?u B"+(j+5)+"))(eps ?z ?u)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(eps ?z B"+(j+10)+")(eps ?u B"+(j+10)+"))(eps ?z ?u)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(eps ?z B"+(j+11)+")(eps ?u B"+(j+11)+"))(eps ?z ?u)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(eps ?z B"+(j+12)+")(eps ?u B"+(j+12)+"))(eps ?z ?u)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(eps ?z B"+(j+13)+")(eps ?u B"+(j+13)+"))(eps ?z ?u)))\n");
				
			} //*/
			
			//* LP15
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being)) " +
					"(<=> (eps ?x ?y)( AND " +
					"(EXISTS ((?z Being)) (eps ?z ?x))" +
					"(FORALL ((?z Being)(?u Being)) (=> (AND(eps ?z ?x)(eps ?u ?x))(eps ?z ?u)))" +
					"(FORALL ((?z Being)) (=> (eps ?z ?x)(eps ?z ?y))))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				
				
			} //*/
			
			//* LP16
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(<=> (j ?x Being_P) (NOT (eps ?x Being_V))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (eps B"+(j+9)+" Being_V))\n");
				
			} //*/
			
			//* LP17
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?z Being)) " +
					"(=> (AND (eps ?x Being_V)(eps ?z ?x)) (eps ?z Being_V)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+1)+" Being_V)(eps ?z B"+(j+1)+")) (eps ?z Being_V)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+5)+" Being_V)(eps ?z B"+(j+5)+")) (eps ?z Being_V)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+9)+" Being_V)(eps ?z B"+(j+9)+")) (eps ?z Being_V)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+11)+" Being_V)(eps ?z B"+(j+1)+")) (eps ?z Being_V)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+19)+" Being_V)(eps ?z B"+(j+19)+")) (eps ?z Being_V)))\n");
				
			} //*/
			
			//* LP18
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (eps ?x ?y)( AND " +
					"(eps ?x ?x)" +
					"(FORALL ((?z Being)) (=> (eps ?z ?x)(eps ?z ?y))))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				
				
			} //*/
			
			//* LP19
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?z Being)) " +
					"(=> (AND (eps ?x Being_V)(eps ?z ?x)) (eps ?x ?z)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+1)+" Being_V)(eps ?z B"+(j+1)+")) (eps B"+(j+1)+" ?z)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+5)+" Being_V)(eps ?z B"+(j+5)+")) (eps B"+(j+5)+" ?z)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+9)+" Being_V)(eps ?z B"+(j+9)+")) (eps B"+(j+9)+" ?z)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+11)+" Being_V)(eps ?z B"+(j+11)+")) (eps B"+(j+11)+" ?z)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+19)+" Being_V)(eps ?z B"+(j+19)+")) (eps B"+(j+19)+" ?z)))\n");
				
			} //*/
			
			//* LP20
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (eps ?x ?y)(<=> (eps ?y Being_V)(eps ?y ?x))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+11)+" Being_V)(eps B"+(j+11)+" B"+(j+10)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+10)+" Being_V)(eps B"+(j+10)+" B"+(j+10)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+12)+" Being_V)(eps B"+(j+12)+" B"+(j+11)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+11)+" Being_V)(eps B"+(j+11)+" B"+(j+12)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+10)+" Being_V)(eps B"+(j+10)+" B"+(j+11)+"))\n");
				
			} //*/
			
			//* LP21
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (eps ?x ?y)(a_ ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+10)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+11)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+12)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+10)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+13)+" B"+(j+13)+")\n");
				
				
			} //*/
			
			//* LP22
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (AND (eps ?x Being_V)(a_ ?x ?y))(eps ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+10)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+11)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+12)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+13)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+14)+" Being_V)\n");
				
			} //*/
			
			//* LP23
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(a_ ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+15)+" B"+(j+15)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+20)+" B"+(j+20)+")\n");
				
			} //*/
			
			//* LP24
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(i_ ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(i_ B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i_ B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i_ B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i_ B"+(j+15)+" B"+(j+15)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i_ B"+(j+20)+" B"+(j+20)+")\n");
				
			} //*/
			
			//* LP25
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (e_ ?x ?y)(NOT (i_ ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (i_ B"+(j+19)+" B"+(j+20)+"))\n");
				
			} //*/
			
			//* LP26
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (o_ ?x ?y)(NOT (a_ ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (a_ B"+(j+1)+" B"+(j+2)+"))\n");
				
			} //*/
			
			//* LP27
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (i_ ?x ?y)(i_ ?y ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(i_ B"+(j+16)+" B"+(j+15)+")\n");
				
			} //*/
			
			//* LP28
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (e_ ?x ?y)(e_ ?y ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(e_ B"+(j+18)+" B"+(j+17)+")\n");
				
			} //*/
			
			writer.close();
		}
	}
	
	@Test
	public final void genLKdata() throws Exception {
		for (int dataSize : scDataSizeArray) {
			
			// data
			
			BufferedWriter writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/lk/data_lk_" + String.format("%05d", dataSize) + ".plm"));
			writer.write("; module-switching\n(IN-MODULE \"/PL-KERNEL-KB/PL-FOUNDATION/PL-SYSTEM/PL-BOUNDARY\")\n");
			writer.write("; assert\n(ASSERT ( AND\n\n");
			
			for (int i = 0; i < dataSize; i++)
				writer.write("\t(Being B" + (i+1) + ")\n");
			writer.write('\n');
			
			int chunks = dataSize/20;
			
			
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				//*
				writer.write("\t(j B"+(j+1)+" B"+(j+2)+")\n");
				writer.write("\t(j B"+(j+2)+" B"+(j+3)+")\n");
				writer.write("\t(j B"+(j+3)+" B"+(j+1)+")\n");
				writer.write("\t(j B"+(j+4)+" Being_U)\n");
				writer.write("\t(eps B"+(j+5)+" Being_U)\n");
				writer.write("\t(j B"+(j+6)+" Being_V)\n");
				writer.write("\t(eps B"+(j+7)+" Being_V)\n");
				writer.write("\t(j B"+(j+8)+" Being_P)\n");
				writer.write("\t(eps B"+(j+9)+" Being_P)\n");
				writer.write("\t(eps B"+(j+10)+" B"+(j+11)+")\n");
				writer.write("\t(eps B"+(j+11)+" B"+(j+12)+")\n");
				writer.write("\t(eps B"+(j+12)+" B"+(j+10)+")\n");
				writer.write("\t(eps B"+(j+13)+" B"+(j+13)+")\n");
				writer.write("\t(eps B"+(j+14)+" B"+(j+14)+")\n");
				writer.write("\t(i_ B"+(j+15)+" B"+(j+16)+")\n");
				writer.write("\t(a_ B"+(j+17)+" B"+(j+18)+")\n");
				writer.write("\t(e_ B"+(j+19)+" B"+(j+20)+")\n");
				writer.write("\t(o_ B"+(j+1)+" B"+(j+2)+")\n");
				//*/
				
				//*/
			}
			writer.write('\n');
			
			writer.write("\n))");
			writer.close();
			
			// exp script
			
			writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/lk/exp_lk_" + String.format("%05d", dataSize) + ".plm"));
			int t = 0;
			int k = 0;
			
			//* LK1
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) (j ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j Being_V Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j Being_P Being_P)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j Being_U Being_U)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+10)+" B"+(j+10)+")\n");
				
			} //*/
				
			//* LK2
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being))" +
				" (=> (AND (j ?x ?y)(j ?z ?x))(j ?z ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+1)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+2)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+3)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+10)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+12)+" B"+(j+11)+")\n");
			} //*/
			
			//* LK3
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?z Being)) " +
					"(=> (AND (j ?x Being_U)(j ?z ?x))(j ?x ?z)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+1)+" Being_U)(j B"+(j+2)+" B"+(j+1)+"))" +
						"(j B"+(j+1)+" B"+(j+2)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+4)+" Being_U)(j B"+(j+5)+" B"+(j+4)+"))" +
						"(j B"+(j+4)+" B"+(j+5)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+10)+" Being_U)(j B"+(j+3)+" B"+(j+10)+"))" +
						"(j B"+(j+10)+" B"+(j+3)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+9)+" Being_U)(j B"+(j+17)+" B"+(j+9)+"))" +
						"(j B"+(j+9)+" B"+(j+17)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+5)+" Being_U)(j B"+(j+5)+" B"+(j+5)+"))" +
						"(j B"+(j+5)+" B"+(j+5)+"))\n");
				
			} //*/
			
			//* LK4
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?z Being)) " +
					"(=> (AND (j ?x Being_U)(j ?z ?x))(j ?z Being_U)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+1)+" Being_U)(j B"+(j+2)+" B"+(j+1)+"))" +
						"(j B"+(j+2)+" Being_U))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+4)+" Being_U)(j B"+(j+5)+" B"+(j+4)+"))" +
						"(j B"+(j+5)+" Being_U))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+10)+" Being_U)(j B"+(j+3)+" B"+(j+10)+"))" +
						"(j B"+(j+3)+" Being_U))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+9)+" Being_U)(j B"+(j+17)+" B"+(j+9)+"))" +
						"(j B"+(j+17)+" Being_U))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(=> (AND (j B"+(j+5)+" Being_U)(j B"+(j+5)+" B"+(j+5)+"))" +
						"(j B"+(j+5)+" Being_U))\n");
				
			} //*/
			
			//* LK5
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(<=> (j ?x Being_U)" +
					"	(FORALL ((?z Being)(?u Being)) (=> (AND(j ?z ?x)(j ?u ?x))(j ?z ?u)))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(j ?z B"+(j+4)+")(j ?u B"+(j+4)+"))(j ?z ?u)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(j ?z B"+(j+5)+")(j ?u B"+(j+5)+"))(j ?z ?u)))\n");
				
				
			} //*/
			
			//* LK6
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (FORALL ((?z Being)) (=> (j ?z ?x)(j ?z ?y)))" +
					"		(FORALL ((?z Being)) (=> (eps ?z ?x)(eps ?z ?y)))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
			} //*/
			
			//* LK7
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(<=> (eps ?x Being_V)(j ?x Being_U)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+4)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+5)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(j B"+(j+7)+" Being_U)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+20)+" Being_V)(j B"+(j+20)+" Being_U))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+6)+" Being_V)(j B"+(j+6)+" Being_U))\n");
				
			} //*/
			
			//* LK8
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being)) " +
					"(=> (AND (eps ?x ?y)(eps ?z ?x))(eps ?z ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+10)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+12)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+11)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+12)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+10)+" B"+(j+10)+")\n");
				
			} //*/
			
			//* LK9
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (eps ?x ?y)(eps ?x ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+11)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+12)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+7)+" B"+(j+7)+")\n");
				
			} //*/
			
			//* LK10
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (eps ?x ?y)(eps ?x Being_V)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+10)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+11)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+12)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+5)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+7)+" Being_V)\n");
				
			} //*/
			
			//* LK11
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being)) " +
					"(=> (AND (eps ?x ?x)(eps ?z ?x))(eps ?x ?z)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+10)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+12)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+11)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+12)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(eps B"+(j+10)+" B"+(j+10)+")\n");
				
			} //*/
			
			//* LK12
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being)) " +
					"(=> (eps ?x ?x)" +
					"(FORALL ((?z Being)(?u Being)) (=> (AND(eps ?z ?x)(eps ?u ?x))(eps ?z ?u)))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(eps ?z B"+(j+5)+")(eps ?u B"+(j+5)+"))(eps ?z ?u)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(eps ?z B"+(j+10)+")(eps ?u B"+(j+10)+"))(eps ?z ?u)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(eps ?z B"+(j+11)+")(eps ?u B"+(j+11)+"))(eps ?z ?u)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(eps ?z B"+(j+12)+")(eps ?u B"+(j+12)+"))(eps ?z ?u)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)(?u Being)) " +
						"(=> (AND(eps ?z B"+(j+13)+")(eps ?u B"+(j+13)+"))(eps ?z ?u)))\n");
				
			} //*/
			
			//* LK13
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being)) " +
					"(<=> (eps ?x ?y)( AND " +
					"(EXISTS ((?z Being)) (eps ?z ?x))" +
					"(FORALL ((?z Being)(?u Being)) (=> (AND(eps ?z ?x)(eps ?u ?x))(eps ?z ?u)))" +
					"(FORALL ((?z Being)) (=> (eps ?z ?x)(eps ?z ?y))))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				
				
			} //*/
			
			//* LK14
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(<=> (j ?x Being_P) (NOT (eps ?x Being_V))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (eps B"+(j+9)+" Being_V))\n");
				
			} //*/
			
			//* LK15
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?z Being)) " +
					"(=> (AND (eps ?x Being_V)(eps ?z ?x)) (eps ?z Being_V)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+1)+" Being_V)(eps ?z B"+(j+1)+")) (eps ?z Being_V)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+5)+" Being_V)(eps ?z B"+(j+5)+")) (eps ?z Being_V)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+9)+" Being_V)(eps ?z B"+(j+9)+")) (eps ?z Being_V)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+11)+" Being_V)(eps ?z B"+(j+1)+")) (eps ?z Being_V)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+19)+" Being_V)(eps ?z B"+(j+19)+")) (eps ?z Being_V)))\n");
				
			} //*/
			
			//* LK16
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (eps ?x ?y)( AND " +
					"(eps ?x ?x)" +
					"(FORALL ((?z Being)) (=> (eps ?z ?x)(eps ?z ?y))))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				
				
			} //*/
			
			//* LK17
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?z Being)) " +
					"(=> (AND (eps ?x Being_V)(eps ?z ?x)) (eps ?x ?z)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+1)+" Being_V)(eps ?z B"+(j+1)+")) (eps B"+(j+1)+" ?z)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+5)+" Being_V)(eps ?z B"+(j+5)+")) (eps B"+(j+5)+" ?z)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+9)+" Being_V)(eps ?z B"+(j+9)+")) (eps B"+(j+9)+" ?z)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+11)+" Being_V)(eps ?z B"+(j+11)+")) (eps B"+(j+11)+" ?z)))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?z Being)) " +
						"(=> (AND (eps B"+(j+19)+" Being_V)(eps ?z B"+(j+19)+")) (eps B"+(j+19)+" ?z)))\n");
				
			} //*/
			
			//* LK18
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (eps ?x ?y)(<=> (eps ?y Being_V)(eps ?y ?x))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+11)+" Being_V)(eps B"+(j+11)+" B"+(j+10)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+10)+" Being_V)(eps B"+(j+10)+" B"+(j+10)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+12)+" Being_V)(eps B"+(j+12)+" B"+(j+11)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+11)+" Being_V)(eps B"+(j+11)+" B"+(j+12)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (eps B"+(j+10)+" Being_V)(eps B"+(j+10)+" B"+(j+11)+"))\n");
				
			} //*/
			
			//* LK19
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (c_ ?x ?y)(c ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
			} //*/
			
			//* LK20
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (a_ ?x ?y)(c_ ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
			} //*/
			
			//* LK21
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (eps ?x ?y)(a_ ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+10)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+11)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+12)+" B"+(j+11)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+10)+" B"+(j+12)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+13)+" B"+(j+13)+")\n");
				
				
			} //*/
			
			//* LK22
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (AND (eps ?x Being_V)(a_ ?x ?y))(eps ?x ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+10)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+11)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+12)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+13)+" Being_V)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+14)+" Being_V)\n");
				
			} //*/
			
			//* LK23
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(a_ ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+15)+" B"+(j+15)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(a_ B"+(j+20)+" B"+(j+20)+")\n");
				
			} //*/
			
			//* LK24
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(i_ ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(i_ B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i_ B"+(j+5)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i_ B"+(j+10)+" B"+(j+10)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i_ B"+(j+15)+" B"+(j+15)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(i_ B"+(j+20)+" B"+(j+20)+")\n");
				
			} //*/
			
			//* LK25
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (e_ ?x ?y)(NOT (i_ ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (i_ B"+(j+19)+" B"+(j+20)+"))\n");
				
			} //*/
			
			//* LK26
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(=> (o_ ?x ?y)(NOT (a_ ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (a_ B"+(j+1)+" B"+(j+2)+"))\n");
				
			} //*/
			
			//* LK27
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (i_ ?x ?y)(i_ ?y ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(i_ B"+(j+16)+" B"+(j+15)+")\n");
				
			} //*/
			
			//* LK28
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)) " +
					"(<=> (e_ ?x ?y)(e_ ?y ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(e_ B"+(j+18)+" B"+(j+17)+")\n");
				
			} //*/
			
			writer.close();
		}
	}

	@Test
	public final void genZLPdata() throws Exception {
		for (int dataSize : scDataSizeArray) {
			
			// data
			
			BufferedWriter writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/zlp/data_zlp_" + String.format("%05d", dataSize) + ".plm"));
			writer.write("; module-switching\n(IN-MODULE \"/PL-KERNEL-KB/PL-FOUNDATION/PL-SYSTEM/PL-BOUNDARY\")\n");
			writer.write("; assert\n(ASSERT ( AND\n\n");
			
			for (int i = 0; i < dataSize; i++)
				writer.write("\t(Being B" + (i+1) + ")\n");
			writer.write('\n');
			
			int chunks = dataSize/20;
			
			
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				//*
				writer.write("\t(sbs B"+(j+1)+" B"+(j+2)+")\n");
				writer.write("\t(sbs B"+(j+2)+" B"+(j+3)+")\n");
				writer.write("\t(sbs B"+(j+3)+" B"+(j+4)+")\n");
				writer.write("\t(sbs B"+(j+4)+" B"+(j+5)+")\n");
				writer.write("\t(sbs B"+(j+5)+" B"+(j+1)+")\n");
				
				writer.write("\t(est B"+(j+6)+" B"+(j+7)+")\n");
				writer.write("\t(est B"+(j+7)+" B"+(j+8)+")\n");
				writer.write("\t(est B"+(j+8)+" B"+(j+9)+")\n");
				writer.write("\t(est B"+(j+9)+" B"+(j+10)+")\n");
				writer.write("\t(est B"+(j+10)+" B"+(j+6)+")\n");
				//*/
				//*
				
				//*/
			}
			writer.write('\n');
			
			writer.write("\n))");
			writer.close();
			
			// exp script
			
			writer = new BufferedWriter(new FileWriter(
					FilePaths.EXP_ROOT + "/zlp/exp_zlp_" + String.format("%05d", dataSize) + ".plm"));
			int t = 0;
			int k = 0;
			
			//* ZLP1
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) (sbs ?x ?x))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(sbs Being_1 Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(sbs Being_0 Being_0)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(sbs B"+(j+1)+" B"+(j+1)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(sbs B"+(j+2)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(sbs B"+(j+3)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(sbs B"+(j+4)+" B"+(j+4)+")\n");
				
			} //*/
				
			//* ZLP2
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being)(?z Being))" +
				" (=> (AND (sbs ?x ?y)(sbs ?z ?x))(sbs ?z ?y)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(sbs B"+(j+1)+" B"+(j+3)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(sbs B"+(j+2)+" B"+(j+4)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(sbs B"+(j+3)+" B"+(j+5)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(sbs B"+(j+4)+" B"+(j+2)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(sbs B"+(j+5)+" B"+(j+3)+")\n");
			} //*/
				
			//* ZLP3
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
					"(<=> (est ?x ?x) (NOT (sbs ?x Being_0))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (sbs B"+(j+6)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (sbs B"+(j+7)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(est B"+(j+8)+" B"+(j+8)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(est B"+(j+9)+" B"+(j+9)+")\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(est B"+(j+10)+" B"+(j+10)+")\n");
			} //*/
				
			//* ZLP4
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
						"(<=> (est ?x Being_1) (NOT (sbs ?x Being_0))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(est B"+(j+6)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(est B"+(j+7)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(est B"+(j+8)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(est B"+(j+9)+" Being_1)\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(est B"+(j+10)+" Being_1)\n");
			} //*/
				
			//* ZLP5
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(est Being_1 Being_1)\n");
			//*/
				
			//* ZLP6
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)) " +
						"(<=> (est ?x Being_1) (est ?x ?x)))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (est B"+(j+6)+" Being_1)(est B"+(j+6)+" B"+(j+6)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (est B"+(j+7)+" Being_1)(est B"+(j+7)+" B"+(j+7)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (est B"+(j+8)+" Being_1)(est B"+(j+8)+" B"+(j+8)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (est B"+(j+8)+" Being_1)(est B"+(j+9)+" B"+(j+9)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(<=> (est B"+(j+1)+" Being_1)(est B"+(j+1)+" B"+(j+1)+"))\n");
			} //*/
				
			//* ZLP7
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					" (<=> (est ?x ?y)(AND (est ?x Being_1)(sbs ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
					
				writer.write("; "+t+"-"+(k++)+"\n\t(AND (est B"+(j+6)+" Being_1)(sbs B"+(j+6)+" B"+(j+7)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(AND (est B"+(j+7)+" Being_1)(sbs B"+(j+7)+" B"+(j+8)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(AND (est B"+(j+7)+" Being_1)(sbs B"+(j+7)+" B"+(j+9)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(AND (est B"+(j+9)+" Being_1)(sbs B"+(j+9)+" B"+(j+7)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(AND (est B"+(j+6)+" Being_1)(sbs B"+(j+6)+" B"+(j+10)+"))\n");
			} //*/
				
			//* ZLP8
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(FORALL ((?x Being)(?y Being))" +
					" (<=> (est ?x ?y)(AND (est ?x ?x)(sbs ?x ?y))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
				
				writer.write("; "+t+"-"+(k++)+"\n\t(AND (est B"+(j+6)+" B"+(j+6)+")(sbs B"+(j+6)+" B"+(j+7)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(AND (est B"+(j+7)+" B"+(j+7)+")(sbs B"+(j+7)+" B"+(j+8)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(AND (est B"+(j+7)+" B"+(j+7)+")(sbs B"+(j+7)+" B"+(j+9)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(AND (est B"+(j+9)+" B"+(j+9)+")(sbs B"+(j+9)+" B"+(j+7)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(AND (est B"+(j+6)+" B"+(j+6)+")(sbs B"+(j+6)+" B"+(j+10)+"))\n");
			} //*/
				
			//* ZLP9
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(REFUTATION-QUERY (FORALL ((?x Being)) (NOT (est Being_0 ?x))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;	
				
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (est Being_0 Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (est Being_0 Being_1))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (est Being_0 "+" B"+(j+1)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (est Being_0 "+" B"+(j+6)+"))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (est Being_0 "+" B"+(j+9)+"))\n");
			} //*/
				
			//* ZLP10
			t++;
			k = 1;
			writer.write("; "+t+"-"+(k++)+"\n\t(REFUTATION-QUERY (FORALL ((?x Being)) (NOT (est ?x Being_0))))\n");
			//*
			for (int i = 0; i < chunks; i++) {
				int j = i * 20;
					
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (est Being_0 Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (est Being_1 Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (est B"+(j+1)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (est B"+(j+6)+" Being_0))\n");
				writer.write("; "+t+"-"+(k++)+"\n\t(NOT (est B"+(j+9)+" Being_0))\n");
			} //*/
				
			writer.close();
		}
	}

}
